A:Type, d:EqDecider(A), i, j:A. i = j  ((eqof(d)(i,j)) ~ true) 

latex

Definitions	Unit, b, b, , P  Q, false, A, False, P  Q, P & Q, P  Q, true, Prop, EqDecider(T), x:A. B(x), t  T, eqof(d)
Lemmas	deq wf, bool sq, bool wf, assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert